#pragma once
#include "PDTExpNumBin.h"
#include "PDTNumConst.h"
#include "PDTTraversalIFC.h"

class PDTAdd :  public PDTExpNumBin, public TraverseIfc <PDTAdd, PDTNode>  { public:  TRAVERSAL_IFC_IMPL(PDTAdd)
public:
	PDTAdd(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTAdd_Em;
	}
	virtual void printType() {
		cout << "PDTAdd_Em";
	}
	bool isAdd() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		int result = child0->getValue() + child1->getValue();
		nValue = new PDTNumConstInt(CG, result);
		cout<<"Addition Result: ("<<child0->getValue()<<") + ("<<child1->getValue()<<") = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTAdd(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "(";
		children[0]->toString(ss) << " + ";
		children[1]->toString(ss) << ")";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTSubt :  public PDTExpNumBin, public TraverseIfc <PDTSubt, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTSubt)
public:
	PDTSubt(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTSubt_Em;
	}
	bool isSubt() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		int result = child0->getValue() - child1->getValue();
		nValue = new PDTNumConstInt(CG, result);
		cout<<"Subtraction Result: ("<<child0->getValue()<<") - ("<<child1->getValue()<<") = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTSubt(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}
	virtual stringstream & toString(stringstream & ss) const {
		ss << "(";
		children[0]->toString(ss) << " - ";
		children[1]->toString(ss) << ")";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);

};

class PDTMult :  public PDTExpNumBin, public TraverseIfc <PDTMult, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTMult)
public:
	PDTMult(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTMult_Em;
	}
	virtual stringstream & toString(stringstream & ss) const {
		ss << "(";
		children[0]->toString(ss) << " * ";
		children[1]->toString(ss) << ")";
		return ss;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		int result = child0->getValue() * child1->getValue();
		nValue = new PDTNumConstInt(CG, result);
		cout<<"Multiplication Result: ("<<child0->getValue()<<") * ("<<child1->getValue()<<") = "<<result<<endl;
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTMult(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	bool isMult() {
		return true;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);

};

class PDTDiv :  public PDTExpNumBin, public TraverseIfc <PDTDiv, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTDiv)
public:
	PDTDiv(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTDiv_Em;
	}
	bool isDiv() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		if (child1->getValue() == 0)
		{
			cout<<"Division by zero failed!"<<endl;
		}
		else
		{
			int result = child0->getValue() / child1->getValue();
			nValue = new PDTNumConstInt(CG, result);
			cout<<"Division Result: ("<<child0->getValue()<<") / ("<<child1->getValue()<<") = "<<result<<endl;
		}
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTDiv(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "(";
		children[0]->toString(ss) << " / ";
		children[1]->toString(ss) << ")";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

class PDTMod :  public PDTExpNumBin, public TraverseIfc <PDTMod, PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTMod)
public:
	PDTMod(PDTCodeGraph & CG, PDTExpNum &left, PDTExpNum & right);
	NodeTypeEnum getType() {
		return PDTMod_Em;
	}
	bool isMod() {
		return true;
	}

	virtual bool eval(PDTCodeGraph &CG)
	{
		children[0]->eval(CG);
		children[1]->eval(CG);
		PDTNumConstInt* child0 = dynamic_cast<PDTNumConstInt*>(children[0]->getNValue());
		PDTNumConstInt* child1 = dynamic_cast<PDTNumConstInt*>(children[1]->getNValue());
		if (child1->getValue() == 0)
		{
			cout<<"Modulo failed: Left operand is zero!"<<endl;
		}
		else
		{
			int result = child0->getValue() % child1->getValue();
			nValue = new PDTNumConstInt(CG, result);
			cout<<"Modulo Result: ("<<child0->getValue()<<") mod ("<<child1->getValue()<<") = "<<result<<endl;
		}
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph &CG)
	{
		PDTNode* toReturn;
		PDTExpNum* childZeroClone = (PDTExpNum*)(children[0]->clone(CG));
		PDTExpNum* childOneClone = (PDTExpNum*)(children[1]->clone(CG));
		toReturn = new PDTMod(CG, *childZeroClone, *childOneClone);
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "(";
		children[0]->toString(ss) << " rem ";
		children[1]->toString(ss) << ")";
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};
